$\forall$$T$:Type, $P$,$Q$:(($T$ List)$\rightarrow$prop\{i:l\}). star{-}append($T$; $P$; $Q$) $\in$ ($T$ List)$\rightarrow$prop\{i:l\}